Introduction in [Giesl and Middeldorp - JFP'04]

Summary: ExIntrod_GM04

• CS-TRS format
• OBJ format
• Negative results:
  1. Lucas' transformation (non-terminating)
  2. Zantema's transformation (non-terminating)
  3. Ferreira and Ribeiro's transformation (non-terminating)
• Positive results:
  1. Giesl and Middeldorp's transformation (Polynomials @ MuTerm)
  2. Polynomial interpretation (MuTerm)
  3. CSRPO
  4. CSDP

CS-TRS ExIntrod_GM04 (file ExIntrod_GM04.csr)

Functions:  nats adx zeros cons 0 incr s hd tl

Constructors:  cons 0 s

Variables:  X Y

Arities: 

ar(nats) = 0
ar(adx) = 1
ar(zeros) = 0
ar(cons) = 2
ar(0) = 0
ar(incr) = 1
ar(s) = 1
ar(hd) = 1
ar(tl) = 1

Replacement map: 

µ(nats)={}
µ(adx)={1}
µ(zeros)={}
µ(cons)={}
µ(0)={}
µ(incr)={1}
µ(s)={}
µ(hd)={1}
µ(tl)={1}

Rules: (file ExIntrod_GM04)  

nats -> adx(zeros)
zeros -> cons(0,zeros)
incr(cons(X,Y)) -> cons(s(X),incr(Y))
adx(cons(X,Y)) -> incr(cons(X,adx(Y)))
hd(cons(X,Y)) -> X
tl(cons(X,Y)) -> Y

The CS-TRS in OBJ format (file ExIntrod_GM04.obj):

obj ExIntrod_GM04 is
  sort S .
  op nats : -> S .
  op adx : S -> S .
  op zeros : -> S .
  op cons : S S -> S [strat (0)] .
  op 0 : -> S .
  op incr : S -> S .
  op s : S -> S [strat (0)] .
  op hd : S -> S .
  op tl : S -> S .
  vars X Y : S .
  eq nats = adx(zeros) .
  eq zeros = cons(0,zeros) .
  eq incr(cons(X,Y)) = cons(s(X),incr(Y)) .
  eq adx(cons(X,Y)) = incr(cons(X,adx(Y))) .
  eq hd(cons(X,Y)) = X .
  eq tl(cons(X,Y)) = Y .
endo

Negative results

1. The mu-termination of ExIntrod_GM04 cannot be proved by using either Lucas', Zantema's, or Ferreira and Ribeiro's transformations [GM04, Section 3].

Positive results

1. The µ-termination of ExIntrod_GM04 can also be proved by using Giesl and Middeldorp's transformation: the TRS ExIntrod_GM04_GM:

       a__nats -> a__adx(a__zeros)
       a__zeros -> cons(0,zeros)
       a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
       a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
       a__hd(cons(X,Y)) -> mark(X)
       a__tl(cons(X,Y)) -> mark(Y)
       mark(nats) -> a__nats
       mark(adx(X)) -> a__adx(mark(X))
       mark(zeros) -> a__zeros
       mark(incr(X)) -> a__incr(mark(X))
       mark(hd(X)) -> a__hd(mark(X))
       mark(tl(X)) -> a__tl(mark(X))
       mark(cons(X1,X2)) -> cons(X1,X2)
       mark(0) -> 0
       mark(s(X)) -> s(X)
       a__nats -> nats
       a__adx(X) -> adx(X)
       a__zeros -> zeros
       a__incr(X) -> incr(X)
       a__hd(X) -> hd(X)
       a__tl(X) -> tl(X)
       

   is terminating (use MuTerm).
2. The µ-termination of ExIntrod_GM04 is proved in [Luc04, Example 3] by using a polynomial interpretation (computed with MuTerm).

       [nats] = 5
       [adx](X) = X + 3
       [zeros] = 1
       [cons](X1,X2) = X1 + 1/2.X2
       [0] = 0
       [incr](X) = X + 1
       [s](X) = 0
       [hd](X) = X + 1
       [tl](X) = 2.X + 1
       

3. The µ-termination of ExIntrod_GM04 can be proved by using CSRPO (proof due to Albert Rubio):
   • marking map:

            m(cons,2)={zeros,incr,adx}=W
            m(incr',1)={zeros,incr,adx}=W
            m(adx',1)={zeros,incr,adx}=W
            

   • precedence:

            nats > adx, zeros
            zeros > cons, 0, zeros'
            incr > cons, s, incr'
            adx > incr, cons, adx'
            tl > zeros, incr, adx
            

   • status:

            st(f) = mul for all function symbols
            

4. The µ-termination of ExIntrod_GM04 can be proved by using CSDP (computed by MuTerm).